\documentclass[a4paper,12pt]{article}

\usepackage{listings}
\usepackage{graphicx}
\usepackage{eso-pic}
\usepackage{fancyhdr}

\author{Y. Fratantonio, A. Bianchi, M. Fossem\'o\\
Mat. 735198, Mat. 734768, Mat. 734531 \\
\small{yanick.fratantonio@gmail.com}\\
\small{antonio.bianchi.333@gmail.com}\\
\small{manuelfossemo@gmail.com}
}
\title{\huge{Automatic Computer-Based Transmission}}
\date{}

\lstset{xleftmargin=-15mm}

\begin{document}



\maketitle

\section{Introduction}
Our work consists in modelling an Automatic Computer-Based Transmission System with TRIO+ language. An automatic transmission is an automobile 
gearbox, that can change gear ratios automatically as the vehicle moves. We have modeled the whole system with the following components: 
the \emph{Engine}, that obviously represents the engine of the car; the \emph{Torque Converter}, that takes the place of a mechanical clutch, 
allowing the load to be separated from the power source; the \emph{Planetary Gear Sets} that are the mechanical systems that provide the various 
forward and reverse gear ratios; the \emph{Wheels} that represents the load of the entire system; the \emph{Hydraulic System} that is a 
transmission system that uses hydraulic fluid under pressure to drive machinery; the \emph{Transmission Control Unit} that is the brain 
of the system that controls the logic which the gears are changed with. Furthermore, we have added to our model three more components 
that are not strictly related with the Automatic Transmission System, but they are very useful to handle the user input. In particular, 
we include the \emph{Throttle} and the \emph{Brake} classes that are useful to handle the user inputs related to the throttle and the 
brake pedal. We also add the \emph{Mode Selector} class that is helpful to handle the user inputs about the drive mode selection: in 
our model the drive modes that the user can select are the Drive mode (D), the Park mode (P), the Reverse mode (R) and the Neutral-No 
Gear mode (N).

\section{Our model}
In this section, we will describe all the TRIO+ classes we have implemented and we will provide a detail explanation for each axiom we have defined.
Furthermore, in the last subsection, we provide a list of facts that our model should guarantee. 

\subsection{Engine}
This class models the engine of the car. Its main function consists in making the drive shaft rotates at a specific rpm.
During normal condition, that is when there are no changes of the current gear, the drive shaft's rpm is defined by the
following relation: \begin{verbatim}rpm(t+1) = f(rpm(t), throttle(t), resistance(t)).\end{verbatim}
Obviously, the rpm(t) term represents the value of the rpm in the t time instant. The throttle(t) term represents how much the 
throttle pedal is pressed: this value is given by the \emph{Throttle} module whose role is to keep how much the throttle pedal 
is pushed. Finally, the resistance(t) term represents how much the engine is obstructed by the external environment: this 
obstruction can be originated, for instance, from the user that has pressed the brake pedal or, from the constant friction between the road 
and the wheels.

On the other hand, when the gear is changed, something different has to happen. In this case we use the following relation:
\begin{verbatim}rpm(t) = f(wheels_speed(t), gear(t)).\end{verbatim} We use this formula in order to simulate the typical behavior of a car 
that makes rpm going down when a gear is changed. However, we have implemented this mechanism without using explicitly the wheels speed and
the gear values: indeed there isn't any explicit link between Engine and Wheels and between Engine and Planetary Gear Set (that is the module
that knows the current gear). The way through which we have modeled this behavior consists in simply don't say anything about the rpm value: 
this value will be setted by the Torque Converter module.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/Engine.png}
\caption{Engine module}
\end{figure}



\footnotesize{
\lstinputlisting{../src/Engine.trio}
}

\normalsize

\subsection{Torque Converter}
The \emph{Torque Converter} module has to connect or disconnect the engine shaft and the shaft that is 
linked with the Planetary Gear Sets module. In our model, this component can be in three different current
states: \emph{connected}, \emph{not connected} and \emph{blocked}. These states are related to the 
drive mode that the user can select: the \emph{connected} state corresponds to the Drive and Reverse 
drive mode, the \emph{not connected} mode corresponds to the Neutral-No gear drive mode, and the \emph{blocked} 
mode corresponds to the Park drive mode.
The selected state represents the state selected with the ModeSelector by the user, it is usually equals to the current state. Selected state changes to x as soon as a change\_torqueMode(x) event occurs. Then also the current state becomes x, except in the following case: if the selected state is \emph{connected} the Torque Converter current state automatically becomes \emph{not connected} if rpm on the shaft linked to Planetary Gear Sets module are lower than a specific threshold (1300).

Here we provide a description about what happens depending on the mode of the Torque Converter.
During normal condition (connected mode) the Torque Converter transfers (with a fixed delay) the rotation of the drive shaft from engine to the planetary gear sets;
in not connected mode, the engine and the planetary gear sets (and so also the wheels) are free to move independently;
finally, in blocked mode, the engine is still disconnected from the planetary gear sets, but the shaft that is connected to the Planetary Gear Sets is blocked,
and as a consequence, wheels are blocked too.
Furthermore, if the engine rpm is lower than a certain threshold, the Torque Converter automatically switches to not connected mode, and viceversa.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/TorqueConverter.png}
\caption{Torque Converter module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/TorqueConverter.trio}
}

\normalsize

\subsection{Planetary Gear Sets}
The purpose of Planetary Gear Sets module is to modify the rotation ratio between the shaft coming from the Torque Converter and the rotation of the wheels.
The relation that is used is the following:\begin{verbatim}out_rpm = in_rpm*ratio(gear).\end{verbatim}
Ratio depends on selected gear and gear is changed according to some signals that are sent by the TCU: in particular, TCU sends a signal that 
indicates how many gears the Planetary Gear Sets has to shift up or down (between -2 and +2).
Furthermore, when changing to Rear, the TCU has to send an additional signal (that, in our TRIO+ code, we call notify\_rear).
The possible gears are: 1,2,3, that represent the forward gears with increasing ratio, while 0 (zero) models the rear gear.
Another important feature is that sequent: changing a gear needs a variable delay between 1 and an upper bound linked to the amount of the shift 
(that can be one or two); Rear gear needs more time to be inserted.
Furthermore, we assume that all the input signals to the Planetary Gear Sets have to be coherent with the current gear 
(for instance no change\_gears(+1) if current\_gear=3): for this reason, we have specified some axioms in the TCU module that prevent 
the arrival of non-sense signals to the Planetary Gear Sets.
The TCU has also to ensure that if any change\_gear event occurs at time t, there won't be other change\_gear events until t+(max possible delay).

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/PlanetaryGear.png}
\caption{Planetary Gear module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/PlanetaryGear.trio}
}

\normalsize

\subsection{Wheels}
This module simply represents the wheels of the car. This is very useful in order to model with a greater level of 
details the whole system. The unique non trivial feature that characterizes this module is the \emph{resistance}. 
With this value we have modeled the friction that is always present between the wheels and the road, and we have 
also modeled the fact that the user can push the brake pedal. For these reasons, we use this relation to set at 
each time instant the value of the resistance: \begin{verbatim}resistance(t) = res_base + brake(t).\end{verbatim}
The \emph{res\_base} value is a constant value that represents the friction, while \emph{brake(t)} value represents
how much the user has pushed the brake pedal in that instant. The other variables that are present in the module
are fundamental but they are very trivial and they don't require any further description in addition to the comments.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/Wheels.png}
\caption{Wheels module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/Wheels.trio}
}

\normalsize

\subsection{Hydraulic System}
The Hydraulic System module has a very trivial behavior. It only has to send the signal that it receive from 
TCU to the Planetary Gear Sets with a delay that can which may vary from one to K time instants. In our case,
this module can only recieve (and send) the \emph{change\_gear} and the \emph{notify\_gear} signals.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/HydraulicSystem.png}
\caption{Hydraulic System module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/HydraulicSystem.trio}
}

\normalsize

\subsection{Transmission Control Unit}
The Transmission Control Unit (TCU) module is one of the most important section of our model, because it manages the 
\emph{logic} of the whole system. Basically, it decides when to change gear according to the actual engine rpm. It
also sends the lock signal to the ModeSelector if wheels speed is too fast, through which we prevent the user to
change the drive mode in a dangerous way (e.g. if the speed is high, the user must not be able to change the drive
mode to Park mode). Now, we provide a brief description about which criteria are used by the controller.
TCU tries to make the engine always works at the best possible rpm (where the torque is max);
it tries to limit the rpm between 2000 and 3000; if rpm are slightly more than 3000, TCU sends the command
change\_gear(+1); if they are slightly less than 2000, it sends the command change\_gear(-1); if rpm are much 
more than 3000 (rpm \textgreater 4000), it sends a change\_gear(+2) signal; if they are much less than 2000 (rpm \textless 1500),
it sends the change\_gear(-2) signal. Obviously the command change\_gear(x) is sent only if \emph{1 \textless = current\_gear + x \textless = 3}.
If correct gear ratios are chosen a change\_gear command makes the wheels rotating at a specific
speed that makes the engine\_rpm always being between 2000 and 3000 rpm after a change gear.
For instance, if ratio of the gear 2 is 1.5 times the ratio of the gear 1, changing from gear 1 
to gear 2 makes the engine rpm equals to the \emph{(engine rpm before the change)/1.5}, but since the 
change from gear 1 to gear 2 can occur only between 3000 and 4000 rpm, the engine rpm after the change 
will be between 2000 and 3000 rpm.
Furthermore, the TCU ensures that if a change\_gear occurs at time t no others
change\_gear can occur until t + \emph{total\_delay}. \emph{total\_delay} should be chosen 
in order to be much bigger than the delay introduced by the hydraulic system and the planetary gear.
Another important aspect of the TCU is the way with which it handles the reverse gear. The main problem is
that the maximum delay that the Planetary Gear Sets need to change the gear is different from a gear to another one.
If the current gear is 1, it is not correct to only send the \emph{change\_gear(-1)} in order to set the reverse gear, but
it also has to specify that the reverse gear is involved. For this reason, we have added to this module the
\emph{notify\_gear} signal. Through this special event, the Planetary Gear Sets know when the reverse gear is involved in
a shift.
Finally, as we said in the \emph{engine} section, the minimum and the maximum limits of the rpm are completely
handled by the engine: the TCU doesn't care with these kind of problems.

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/TCU.png}
\caption{Transmission Control Unit module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/TCU.trio}
}

\normalsize

\subsection{Throttle}
The Throttle module is quite simple. It deals with the problem of handling the user inputs. In particular, this module
handles inputs that are related with the throttle pedal. The behavior of this module is the following: if exists a value 
that makes the throttle\_pedal event true (that is the throttle pedal is pushed), than it has to modify coherently 
the throttle\_signal; otherwise, if the user does not push the throttle pedal, the value of the throttle\_signal has 
to be equal to zero. The throttle\_signal variable is useful in order to calculate the value of the engine rpm.

\begin{figure}
\centering
\includegraphics[scale=0.7]{images/Throttle.png}
\caption{Throttle module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/Throttle.trio}
}

\normalsize

\subsection{Brake}
The Brake module is very similar to the Throttle module. One of the two difference is that this module has to handle the brake pedal.
Its behavior is analogous with respect to the one described in the previous section: if exists a value that makes 
the brake\_pedal event true (that is the brake pedal is pushed), than it has to modify coherently the 
throttle\_singal; otherwise, if the user does not push the brake pedal, the value of the brake\_pedal 
has to be equal to zero. Furthermore, the brake\_signal variable is linked to the Wheels: an high brake\_signal value increases
the \emph{resistance} variable (in the Wheels module) and it indirectly decreases the speed of the car, that is
purpouse of the Brake module.

\begin{figure}
\centering
\includegraphics[scale=0.7]{images/Brake.png}
\caption{Brake module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/Brake.trio}
}

\normalsize

\subsection{Mode Selector}
The Mode Selector module is one of the most important of the whole system. Its purpose is to handle the inputs from the user
that are related with the drive mode. As we said before, our system is able to model four different drive mode: the Drive (D),
the Park (P), the Reverse (R) and the Neutral-No gear (N) mode. The main reason that brings us to add this module is that 
the system must not always follow the user inputs, because, in some extreme situations, it could happen something dangerous. 
For instance, if the car is moving at high speed and the user tries to switch from the D mode to the P mode, 
the system has to ignore the user wish and it has to remain in the D mode.
In order to implement this behavior, we have added to this module the \emph{lock} state variable. This variable is controlled
and modified by the TCU that decides when the user can shift from one drive mode to an other one. The TCU can modify this
variable using \emph{lock\_mode} and \emph{unlock\_mode} signals. This module also communicate with the Torque Converter
module through the \emph{change\_torqueMode} event, in order to modify coherently the torque converter mode (that can be
\emph{connected}, \emph{not connected} and \emph{blocked}).

\begin{figure}
\centering
\includegraphics[scale=0.6]{images/ModeSelector.png}
\caption{Mode Selector module}
\end{figure}

\footnotesize{
\lstinputlisting{../src/ModeSelector.trio}
}

\normalsize

\subsection{Transmission}
It represents the connection between all the components and between the model and the external environment. In our formalization the connections between the model and the external enviromental are: the user actions on the throttle and the brake pedal; the user actions that are related with the mode selector (through which the user 
choose the drive mode from Drive, Reverse, Park and Neutral-No Gear); the speed of the wheels that represents a sort of output. In the last page, we provide a draw that shows how all the modules are connected one with each other.

\subsection{Requirements}
The whole system must guarantee the following requiremets:

- the wheels speed must not change too fast, because this can damage the car.

Alw(wheels\_speed = x -\textgreater (Dist(wheels\_speed = x + t,1)\& (-10  \textless t  \textless 10)))
\\\\
- the engine rpm must always be in a specific range (between 1000 and 5000).

Alw( 1000  \textless = engine\_rpm  \textless = 5000)
\\\\
- the engine rpm should be whenever it is possible between 2000 and 3000 (at least after a change gear).

Alw( notify\_change\_gear -\textgreater (2000  \textless engine\_rpm  \textless 3000))

\clearpage
\pagestyle{empty}

\AddToShipoutPicture*{%
\put(20,40){\includegraphics[angle=90, width=200mm]{images/Trio.png}}%
}



\clearpage
\verb| |



\clearpage

\section{Model checking}
In this section, we describe our work related to model checking. We decide to check the model with both the tools that are available, that are Trio2Promela and Zot. We have encountered many difficulties in using these tools because they are not well documented and we have found some bugs that have increased our troubles. Because of these problems, we managed to check only trivial properties that are quite similar to our axioms, but we have learned how the model check is performed.

\subsection{Trio2Promela}
It has been very difficult to use this tool in the right way. The main problem is that it happens that the tool makes some mistakes in the translation from TRIO to Promela, and it doesn't warn the user about this fact: this is terrible! But once we have learned in which way we can use the tool (thanks to a great support of the TA), we have been able to test some (simple) properties of our model.
Given the model, there are two ways to make some model checks with this tool. The first one consists in specifying a LTL property that has to be derivable from the axioms of the model. The second one is a little bit trickier, because we have to negate the theorem we want to prove and we have to add it to our axioms. Then if the resulting model is unfeasible, the theorem is proved.
Here we provide the simplification of the TRIO code that is used to verify some simple properties related to the \emph{Mode Selector}, the \emph{Torque Converter} and the \emph{Hydraulic System} modules.

\lstset{xleftmargin=-15mm}

\footnotesize{
\lstinputlisting[frame=single,framexrightmargin=15mm,caption=ModeSelector.t2p]{../t2p/ModeSelector1.t2p}
\lstinputlisting[frame=single,framexrightmargin=15mm,caption=Torque Converter.t2p]{../t2p/Torque1.t2p}
\lstinputlisting[frame=single,framexrightmargin=15mm,caption=Hydraulic System and Planetary Gear Sets.t2p]{../t2p/Hydraulic.t2p}
}

\normalsize
\subsubsection{Model check with LTL properties}
Using the LTL, we have verified two simple propreties of the \emph{Mode Selector} moduel. The first is:
\begin{verbatim}
(lock==1 && user_change_driveMode!=N) ->
   (notify_driveMode==0 && change_torqueMode==0)
\end{verbatim}
The meaning of this property is the following: if \verb|lock==1| then all \verb|the user_change_driveMode| that are different from the Neutral-No gear mode have to ignored. Notice that we don't say anything about the value of the current gear at next time instant: indeed it is very hard to test something in different time instant with the LTL, because the \emph{next} operator is not supported. Anyway, we have checked these trivial properties with the second technique.
The second property we have verified is:
\begin{verbatim}
(user_change_driveMode==D && lock==0) -> 
   (change_torqueMode==Connected && notify_driveMode=D)
\end{verbatim}
This formula means that the \emph{Torque Mode} has to be coherent with the \emph{Drive Mode} that has been selected.
The second module we have checked with the LTL is the \emph{Torque Converter} module. Also in this case, we have verified two simple properties.
The first is:
\begin{verbatim}
(in_rpm<=1 && selected_TorqueMode==Connected) ->
   (current_TorqueMode==NotConnected)
\end{verbatim}
In this case, \emph{one rpm} represents the threshold from which the torque converter has to disconnect the engine and the load.
The second is:
\begin{verbatim}
(out_rpm>=2) -> 
   (selected_TorqueMode==Connected || selected_TorqueMode==NotConnected)
\end{verbatim}
This last property aims to check that if the \emph{out\_rpm} are greater or equal than 2, the Torque Converter can not be in the \emph{Blocked} mode.

\subsubsection{Model check through negated axioms}
In order to check some properties that are related to different time instant, we have to use the second technique.
The first theorem that we have proved (related to the ModeSelector) is the following:
\begin{verbatim}
Past(user_change_driveMode=D & lock=0,1) -> current_driveMode = D
\end{verbatim}
In order to prove this formula, we have added to our model the sequent axiom, that is the negation of the previous theorem:
\begin{verbatim}
Now(SomF( Past(user_change_driveMode=D,1) & 
                                Past(lock=0,1) & current_mode<>D));
\end{verbatim}
Then we have determined that the new model is not feasible by specifying the
\begin{verbatim}
[]<>!np_ -> <> (!s1 && t1)
\end{verbatim} LTL formula. We have finished our prove by obtaining the VALID answer from SPIN.

The second theorem related to the Mode Selector that we have proved is the following:
\begin{verbatim}
Past(user_change_driveMode=P & lock=1 & current_mode=D, 1) -> 
                                                  current_mode = D;
\end{verbatim}
This formula says that if, for example, the current mode is \emph{Drive} and the user tries to change the mode to \emph{Park} when the lock variable is setted to one, the value of the current mode in the next time instant has to be the same of the previous instant.
In this case, we have added to our model the sequent formula:
\begin{verbatim}
Now(SomF( Past(user_change_driveMode=P,1) & Past(lock=1,1) & 
                        Past(current_mode=D,1) & current_mode<>D));
\end{verbatim}
The last property that we have verified is related to the Hydraulic System and the Planetary Gear Sets modules. The situation is the following: the TCU sends a change\_gear signal to the Hydraulic System; the Hydraulic System takes at most \emph{HydSystemDelay} time instants to propagate this signal to the Planetary Gear Sets; the Planetary Gear Sets, when it receives a change\_gear signal, it has to physically change the gear; the Planetary Gear Sets takes at most \emph{PlanetaryGearDelay} to change the gear and to send to the whole system the \emph{notify\_change\_gear} signal. The theorem that we have proved is the sequent: if in the time instant \emph{t} the TCU raised the change\_gear signal, the Planetary Gear Sets has to raise the \emph{notify\_change\_gear} in at most \emph{HydSystemDelay + PlanetaryGearDelay}.
This theorem is represented by the following formula:
\begin{verbatim}
in_change_gear=sh & sh<>0 -> 
   WithinF(notify_change_gear=1,HydSystemDelay + PlanetaryGearDelay);
\end{verbatim}
As in the previous cases, we have to add to the model the negation of this formula, that is the seguent:
\begin{verbatim}
Now(SomF(Past(in_change_gear=sh,4) & Past(sh<>0,4) & 
        Past(notify_change_gear=1,3) & Past(notify_change_gear=1,2) &
        Past(notify_change_gear=1,1) & notify_change_gear=1));
\end{verbatim}
\subsection{ZOT}
We use Zot to model and check some properties of the system related to the TorqueConverter, the Engine and the ModeSelector.
In particular we have verified the relationship between the engine rpm (rpm\_in), rpm from TorqueConverter to Planetary Gear Sets (rpm\_out) and selected mode.
We have only verified time-independent properties, in this way we have less constraints about the cardinality of the domains,
that can be much more similar to that of the original TRIO+ model.

In order to understand better our work, please refer to the file zot\_model.lisp, that is included at the end of this section.
In axiom's comments it is written which is the corresponding axiom in TRIO+ model.

After checking the satisfiability of the model, we prove that a theorem can be derived from the original model,
if the new model, created adding the negation of theorem, is unsatisfiable.\\

The theorems we have proved are the following:\\
\begin{itemize}
\item \emph{not\_connected\_if\_low\_rpm\_in\_or\_low\_rpm\_out} and \emph{low\_or\_high\_rpm\_out\_only \_if\_not\_connected}
We check that if the rpm\_out are too low or too high for the engine, the torque converter is not in connected state,
so the engine is disconnected from the wheels. In other words we check that when the engine is connected to the wheels,
rpm are always suitable for the engine. Notice that if the rpm\_out are equal to zero the TorqueConverter can be either
in NotConnected or Blocked state.

\item \emph{car\_moving\_if\_DorR}
We check that if the selected mode is D or R and the actual engine rpm are sufficiently high the rpm\_out are greater than zero,
so the car is moving.

\item \emph{car\_blocked\_if\_P}
We check that if the selected mode is Parking the rpm\_out are equal to zero and so the car is not moving.
\end{itemize}

Running Zot with only the axioms it tells us that the model is satisfiable and it also shows some possible assignment for the variables.
For instance:
\begin{verbatim}
  RPM_IN_1.5
  DM_D
  SM_C
  CM_C
  RPM_OUT_1.5
\end{verbatim}
Engine rpm are 1500, the car is in Drive mode, engine and wheels are connected and rpm\_out are 1500 as engine rpm.
\begin{verbatim}
  RPM_IN_1.5
  DM_R
  SM_C
  CM_C
  RPM_OUT_1.5
\end{verbatim}  
Engine rpm are 1500, the car is in Rear mode, engine and wheels are connected and rpm\_out are 1500 as engine rpm.
(Notice that rpm\_out are still positive because the inversion of the shaft movement is done by the Planetary Gear Sets)
\begin{verbatim}
  RPM_IN_1.5
  DM_P
  SM_B
  CM_B
  RPM_OUT_0
\end{verbatim}
Engine rpm are 1500, the car is in Parking mode, so rpm\_out are zero (the car is blocked).
\begin{verbatim}
  RPM_IN_1.1
  DM_D
  SM_C
  CM_NC
  RPM_OUT_2
\end{verbatim}
Engine rpm are 1100, the car is in Drive mode, so TorqueConverter is NotConnected (1100<1300).
When TorqueConverter is not connected the engine rpm and rpm\_out are not related in any way.
In this case rpm\_out is 2000.

The last example shows a possible unwanted behavior of the model. Since the engine rpm are below a specific threshold (1300),
the TorqueConverter is not connected and engine rpm and rpm\_out are not related. So it possible for rpm\_out to have
any value. This physically means that if the engine rpm are too low the car is free to move with any speed (eventually zero).
In real world this is not strictly true because of the engine breaking action. Anyway model this kind of behavior is very complicated with
a logic oriented language such as TRIO+, so, for this reason, we prefer to model the action of the wheels on the engine with a variable (resistance) and forcing
the engine rpm according to the wheels speed only when a gear is changed.

\footnotesize{
\lstinputlisting[caption=zot\_model]{../zot/zot_model.lisp}
}
\normalsize

\end{document}
